A:es_realizer{i:l}. R-discrete_compat(A; A) 

latex

Definitions	x. t(x), ff, prop{i:l}, tt, t  T, True, P  Q, if b then t else f fi , R-discrete_compat(A; B), es_realizer{i:l}, x:A. B(x), x(s), P  Q, P  Q, Unit, ,
Lemmas	finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, unit wf, Rinit-x wf, Rinit-discrete wf, Rinit? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Reffect-x wf, Id wf, Reffect-discrete wf, eqtt to assert, bool wf, Reffect? wf